(declare-fun _substvar_41_ () (_ BitVec 3))
(declare-fun _substvar_62_ () (_ BitVec 3))
(declare-fun v6 () Bool)
(declare-fun _3-0 () (_ BitVec 3))
(assert (or (= _substvar_62_ _3-0 _substvar_41_ (_ bv0 3)) (= (= (_ bv0 3) _3-0 (bvsdiv _3-0 _3-0) (_ bv0 3)) v6 true true true)))
(check-sat)
(declare-fun X () (_ FloatingPoint 2 6))
(declare-fun Y () (_ FloatingPoint 2 6))
(declare-fun Z () (_ FloatingPoint 2 6))
(declare-fun W () (_ FloatingPoint 2 6))
(assert (and (distinct X (fp.mul RTZ Y Z)) (distinct X (fp.sub RTZ Y Z)) (= X (fp.div RTZ Y Z)) (= X (fp.add RTZ Y Z)) (= X (fp.fma RTZ Y Z W)) (= X (fp.sqrt RTZ Y)) (distinct X (fp.rem X Y)) (distinct X (fp.roundToIntegral RTZ Y)) (distinct X (fp.max Y Z)) (distinct X (fp.min Y Z))))
(check-sat)
(declare-fun _substvar_508_ () Int)
(declare-fun ALU (Int Int Int) Int)
(assert (not (= (ALU 0 0 0) (ALU 0 (ite false 0 _substvar_508_) 0))))
(check-sat)
